1. $T$ : Type
\\[0ex]2. $L$ : $T$ List
\\[0ex]3. $x$ : $T$
\\[0ex]4. $y$ : $T$
\\[0ex]5. adjacent($T$;$L$;$x$;$y$)
\\[0ex]6. $x$ before $y$ $\in$ $L$
\\[0ex]7. ($y$ $\in$ $L$)
\\[0ex]8. ($x$ $\in$ $L$)
\\[0ex]$\vdash$  \{($x$ $\in$ $L$) \& ($y$ $\in$ $L$)\}